es:ES, P:(E).
(e:E. Dec(P(e)))  (e:E. P(e)  (m:E. (m c e & P(m) & (e':E. (e' < m)  (P(e')))))) 

latex

Definitions	A, P  Q, e c e', A c B, x. t(x), P & Q, x:A. B(x), P  Q, t  T, x(s), x:A. B(x), , False, Dec(P)
Lemmas	es-le weakening eq, es-causle weakening locl, es-causle weakening, es-causl transitivity1, decidable existse-causl, event system wf, decidable wf, not wf, es-causl wf, es-causle wf, es-E wf